$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$, ${\it da}$:$k$:Knd fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$, $P$:(ecl(${\it ds}$;${\it da}$)$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$).
\\[0ex]($\forall$$k$:Knd, ${\it test}$:(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow\mathbb{B}$). $P$(eclbase($k$;${\it test}$)))
\\[0ex]$\Rightarrow$ ($\forall$$a$, $b$:ecl(${\it ds}$;${\it da}$). $P$($a$) $\Rightarrow$ $P$($b$) $\Rightarrow$ $P$(eclseq($a$;$b$)))
\\[0ex]$\Rightarrow$ ($\forall$$a$, $b$:ecl(${\it ds}$;${\it da}$). $P$($a$) $\Rightarrow$ $P$($b$) $\Rightarrow$ $P$(ecland($a$;$b$)))
\\[0ex]$\Rightarrow$ ($\forall$$a$, $b$:ecl(${\it ds}$;${\it da}$). $P$($a$) $\Rightarrow$ $P$($b$) $\Rightarrow$ $P$(eclor($a$;$b$)))
\\[0ex]$\Rightarrow$ ($\forall$$a$:ecl(${\it ds}$;${\it da}$). $P$($a$) $\Rightarrow$ $P$([$a$]$\ast$))
\\[0ex]$\Rightarrow$ ($\forall$$a$:ecl(${\it ds}$;${\it da}$), $n$:$\mathbb{N}$. $P$($a$) $\Rightarrow$ $P$($a$.$n$))
\\[0ex]$\Rightarrow$ ($\forall$$a$:ecl(${\it ds}$;${\it da}$), $n$:$\mathbb{N}$. $P$($a$) $\Rightarrow$ $P$(eclthrow($a$;$n$)))
\\[0ex]$\Rightarrow$ ($\forall$$a$:ecl(${\it ds}$;${\it da}$), $l$:$\mathbb{N}$ List. $P$($a$) $\Rightarrow$ $P$(eclcatch($a$;$l$)))
\\[0ex]$\Rightarrow$ \{$\forall$$x$:ecl(${\it ds}$;${\it da}$). $P$($x$)\}